<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html; charset=ISO-8859-1"
 http-equiv="content-type">
  <title>BottomUpProving-ByNormMegill</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
 vlink="#ff0000" alink="#000088" link="#0000ff">
<big><big><span style="font-weight: bold;">Bottom-Up Proving by Norm
Megill<br>
<br>
</span></big></big><big><span style="font-weight: bold;">See also:<br>
</span></big><a href="PAUserGuide/Start.html">Proof Assistant User Guide</a><br>
<a href="ProofAssistantGUIQuickHOWTO.html">ProofAssistantGUIQuickHOWTO.html</a><br>
<a href="ProofAssistantGUIDetailedInfo.html">ProofAssistantGUIDetailedInfo.html</a><br>
<a href="ProofAssistantGUIDeriveFeature.html">ProofAssistantGUIDeriveFeature.html</a><br>
<a href="StepUnifier.html">StepUnifier.html</a><br>
<a href="../mmj2jar/PATutorial/PageLocalRef.mmp">PageLocalRef.mmp</a><br>
<a href="WorkVariables.html">WorkVariables.html</a><br>
<a href="StepSelectorSearch.html">StepSelectorSearch.html</a><br>
<a href="UnifyEraseAndRederiveFormulasFeature.html">UnifyEraseAndRederiveFormulas.html</a><br>
<br>
<hr style="width: 100%; height: 2px;"><br>
<h3>Quick Tip:&nbsp; mmj2 for Metamath Solitaire Users</h3>
With the advent of "work variables", the latest releases of mmj2 have
hidden inside of them the same algorithm that <a
 href="http://us2.metamath.org:8888/mmsolitaire/mms.html">Metamath
Solitaire</a> uses for its unification. (Well, the algorithm may be
different, but I mean the same in terms of its outcome.)<br>
<br>
So, it is possible to emulate Metamath Solitaire with mmj2.&nbsp; And
unlike the Metamath Solitaire applet, you can save a partially
completed proof to continue to work on later.&nbsp; In addition, mmj2
not only can be used to create proofs forward as Metamath Solitaire
does, it can also be used to create them backwards from the conclusion.<br>
<br>
<h3>Backwards proof example</h3>
I'll start with a backwards proof example, since it can be entered
"blindly" from an existing Metamath Solitaire proof in a very simple
manner.<br>
<br>
I'll start at the beginning, assuming you are using Windows, so you
won't have to read the mmj2 documentation.&nbsp; Download the latest <code><a
 href="http://us2.metamath.org:8888/index.html#mmj2">mmj2.zip</a></code>
and put it in <code>c:\mmj2.zip</code>.&nbsp; Extract the Zip file to
create <code>c:\mmj2</code> with default settings.&nbsp; From the
result, move or copy the directory <code>c:\mmj2\mmj2jar</code> to <code>c:\mmj2jar</code>
(run <code>c:\mmj2\mmj2jar\copymmj2jar.bat</code> to create and copy <code>c:\mmj2jar</code>
-- see below for instructions on running a "<code>.bat</code>" file.)<br>
<br>
I assume you have Java installed.&nbsp; If not, I guess you'll have to
read the mmj2 documentation after all.<br>
<br>
Next, download <a href="http://us2.metamath.org:8888/metamath/set.mm">set.mm</a>
(6MB) into the directory <code>c:\metamath</code>.&nbsp; Or, if you
want it somewhere else, change the parameter <br>
<br>
<code style="font-weight: bold;">&nbsp; LoadFile,set.mm</code><br>
<br>
accordingly, using a text editor like Notepad to edit<br>
<br>
<code style="font-weight: bold;">&nbsp;&nbsp; c:\mmj2jar\RunParms.txt</code><br>
<br>
You may also need to update the "mmj2Path" parameter in mmj2.bat
(command line argument #3 after "<code>mmj2.jar</code>") in:<br>
<br>
<code style="font-weight: bold;">&nbsp;&nbsp; c:\mmj2jar\mmj2.bat<br>
<br>
Then<br>
</code><br>
In Windows, select Start -&gt; Run, type "<code>cmd</code>", click OK,
and a Command Prompt window will open.&nbsp; Type <br>
<br>
<code style="font-weight: bold;">&nbsp; c:\mmj2jar\mmj2.bat</code><br>
<br>
following by Enter to start mmj2.<br>
<br>
<span style="color: rgb(0, 153, 0); font-weight: bold;">NOW set mmj2's
ProofAsstGUI screen Edit/Set Incomplete Step Cursor menu
item to "3" - Last.</span><br>
<br>
A useful reference file for playing with Metamath Solitaire is the
http://us2.metamath.org:8888/mmsolitaire/pmproofs.txt <a
 href="http://us2.metamath.org:8888/mmsolitaire/pmproofs.txt">pmproofs.txt</a>
- Shortest known proofs list.&nbsp; Each of the 193 proofs begins with
two lines:&nbsp; the theorem itself and the "Result of proof" when you
enter the proof into the Metamath Solitaire applet.&nbsp; The "Result
of proof" line is what you want to focus on:&nbsp; the theorem itself
often requires the introduction of definitions, which is beyond the
scope of this tutorial and is an exercise for advanced users.<br>
<br>
It turns out that all of these 193 theorems also exist in set.mm.&nbsp;
Most of them have definitions incorporated and don't match the "Result
of proof".&nbsp; But some of them do, such as set.mm's "<code>imim2</code>"
for
theorem
"*2.05
Syll".&nbsp; So for this example, we will pick that
one, since it is already in set.mm and we won't have to type it in.<br>
<br>
From the mmj2 ProofAsstGUI screen, select File -&gt; New Proof -&gt;
imim2.<br>
The screen will look like this:<br>
<br>
<code style="font-weight: bold;">&nbsp;$( &lt;MM&gt; &lt;PROOF_ASST&gt;
THEOREM=imim2&nbsp; LOC_AFTER=?<br>
<br>
&nbsp;* A closed form of syllogism (see ~ syl ).&nbsp; Theorem *2.05 of<br>
&nbsp;&nbsp; [WhiteheadRussell] p. 100.<br>
<br>
&nbsp;qed::&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|-
(
(
ph -&gt; ps ) -&gt; ( ( ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) )<br>
<br>
&nbsp;$)<br>
</code><br>
We can see that the "<code>qed</code>" step matches the "Result of
proof" for theorem "*2.05 Syll", which is what we want.&nbsp; (For
other proofs where it doesn't, we can change the qed step so that it
does.)<br>
<br>
Look at the proof in the pmproofs.txt file:<br>
<br>
<code><span style="font-weight: bold;">&nbsp; DD2D121; ! 7 steps</span></code><br>
<br>
Unlike the Metamath Solitaire applet, we are going to enter this proof
from left-to-right instead of right-to-left.&nbsp; The letter D means
ax-mp, 2 means ax-2, and 1 means ax-1.<br>
<br>
On the mmj2 ProofAsstGUI screen, the cursor should be
positioned immediately after the second colon in "<code>qed::</code>".&nbsp;
Here
are
the
exact stepsto enter the proof, following the "<code>DD2D121</code>"
above
exactly:<br>
<br>
Type <code>ax-mp</code> (just the 5 characters "ax-mp" with no Enter),
ctrl-u (hold down the ctrl key and press "u"), <code>ax-mp</code>,
ctrl-u, <code>ax-2</code>, ctrl-u, <code>ax-mp</code>, ctrl-u, <code>ax-1</code>,
ctrl-u,
<code>ax-2</code>, ctrl-u, <code>ax-1</code>, ctrl-u.&nbsp;
Voila, the proof is done and will look like this:<br>
<br>
<code style="font-weight: bold;">&nbsp;$( &lt;MM&gt; &lt;PROOF_ASST&gt;
THEOREM=imim2&nbsp; LOC_AFTER=?<br>
<br>
&nbsp;* A closed form of syllogism (see ~ syl ).&nbsp; Theorem *2.05 of<br>
&nbsp;&nbsp; [WhiteheadRussell] p. 100.<br>
<br>
&nbsp;1000::ax-1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|-
(
(
ph -&gt; ps ) -&gt; ( ch -&gt; ( ph -&gt; ps ) ) )<br>
&nbsp;5000::ax-2&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; |-
(&nbsp; ( ch -&gt; ( ph -&gt; ps ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) )<br>
&nbsp;6000::ax-1&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; |-
(&nbsp; (&nbsp; ( ch -&gt; ( ph -&gt; ps ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(&nbsp;
(
ph -&gt; ps )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(&nbsp;
(
ch -&gt; ( ph -&gt; ps ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) ) ) )<br>
&nbsp;3000:5000,6000:ax-mp<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|-
(&nbsp;
(
ph -&gt; ps )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(&nbsp;
(
ch -&gt; ( ph -&gt; ps ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) ) )<br>
&nbsp;4000::ax-2&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; |-
(&nbsp; (&nbsp; ( ph -&gt; ps )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(&nbsp;
(
ch -&gt; ( ph -&gt; ps ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(&nbsp;
(
( ph -&gt; ps ) -&gt; ( ch -&gt; ( ph -&gt; ps ) ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(&nbsp;
(
ph -&gt; ps )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) ) ) )<br>
&nbsp;2000:3000,4000:ax-mp<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
|-
(&nbsp;
(
( ph -&gt; ps ) -&gt; ( ch -&gt; ( ph -&gt; ps ) ) )<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
-&gt;
(
(
ph -&gt; ps ) -&gt; ( ( ch -&gt; ph ) -&gt; ( ch -&gt; ps ) )
) )<br>
&nbsp;qed:1000,2000:ax-mp&nbsp;&nbsp;&nbsp;&nbsp; |- ( ( ph -&gt; ps )
-&gt; ( ( ch -&gt; ph ) -&gt; ( ch -&gt; ps ) ) )<br>
<br>
&nbsp;$=&nbsp; wph wps wi wch wph wps wi wi wi wph wps wi wch wph wi
wch wps wi<br>
&nbsp;&nbsp;&nbsp;&nbsp; wi wi wph wps wi wch ax-1 wph wps wi wch wph
wps wi wi wch wph wi<br>
&nbsp;&nbsp;&nbsp;&nbsp; wch wps wi wi wi wi wph wps wi wch wph wps wi
wi wi wph wps wi wch<br>
&nbsp;&nbsp;&nbsp;&nbsp; wph wi wch wps wi wi wi wi wch wph wps wi wi
wch wph wi wch wps wi<br>
&nbsp;&nbsp;&nbsp;&nbsp; wi wi wph wps wi wch wph wps wi wi wch wph wi
wch wps wi wi wi wi<br>
&nbsp;&nbsp;&nbsp;&nbsp; wch wph wps ax-2 wch wph wps wi wi wch wph wi
wch wps wi wi wi wph<br>
&nbsp;&nbsp;&nbsp;&nbsp; wps wi ax-1 ax-mp wph wps wi wch wph wps wi wi
wch wph wi wch wps wi<br>
&nbsp;&nbsp;&nbsp;&nbsp; wi ax-2 ax-mp ax-mp $.<br>
&nbsp;$)<br>
</code><br>
<span style="font-style: italic;">[Forward Proving Narrative excised by
editor]</span><br>
<br>
As a final note, it is sometimes interesting to see if the proof as a
whole leads to a more general theorem than the one shown by the '<code>qed</code>'
step.&nbsp;
To
do
that, just add the last <code>ax-mp</code> in its
own new step instead of modifying the '<code>qed</code>' step.&nbsp; In
this example, a more general theorem does not result, as you can verify
as an exercise.<br>
<br>
-- Norm 22 Jan 2008.<br>
<br>
</body>
</html>
